Rsends(${\it ds}$; ${\it knd}$; $T$; $l$; ${\it dt}$; $g$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr inr inr inr inr inr (inl $<$${\it ds}$, ${\it knd}$, $T$, $l$, ${\it dt}$, $g$$>$ )